#Functional Programming

[track-maniac]

Feeling inspired by a post I saw a few months ago, I programmed a simple game of tic-tac-toe in python, in a single expression. Like regular functional programming, this means I can't mutate variables. But more than functional programming, this also means I can't

Declare variables at all

Declare functions

Use most loops and branch structures

The resulting program is 1730 characters long after removing all the non-strictly necessary whitespace and contains "lambda" 9 times.

The players are asked where they want to play using a number for each cell, in the configuration of a standard numpad. The program checks for invalid input too.

Source code under the cut

(lambda grid,toggle,players,cells_filled,print_grid,check_victory,ask_xy,validate_input,the_game:(lambda victor:print('=====\n'+('Draw.'if victor is None else f"{victor} wins!")))(the_game(grid,players,cells_filled,toggle,print_grid,check_victory,ask_xy,validate_input,the_game)))([[7,8,9],[4,5,6],[1,2,3]],True,['X','O'],0,lambda grid:print('\n'+'\n'.join(' '.join(map(str,ligne))for ligne in grid)),lambda grid,players:([player for player in players if any(set(grid[i][col]for i in[0,1,2])=={player}for col in[0,1,2])or any(set(grid[row])=={player}for row in[0,1,2])or set(grid[i][i]for i in[0,1,2])=={player}or set(grid[i][2-i]for i in[0,1,2])=={player}]+[None])[0],lambda players,toggle,grid,ask_xy,validate_input:validate_input(input(f"{players[toggle]}, place your symbol: "),grid,players,toggle,ask_xy,validate_input),lambda selection,grid,players,toggle,ask_xy,validate_input:(lambda selection,grid,players,toggle,ask_xy,validate_input:(selection%3,2-selection//3)if grid[2-selection//3][selection%3]not in players else ask_xy(players,toggle,grid,ask_xy,validate_input))(int(selection)-1,grid,players,toggle,ask_xy,validate_input)if len(selection)==1 and'0'<selection<='9'else ask_xy(players,toggle,grid,ask_xy,validate_input),lambda grid,players,cells_filled,toggle,print_grid,check_victory,ask_xy,validate_input,the_game:(print_grid(grid),the_game((lambda players,toggle,xy,grid:[[players[not toggle]if(j,i)==xy else grid[i][j]for j in[0,1,2]]for i in[0,1,2]])(players,toggle,ask_xy(players,not toggle,grid,ask_xy,validate_input),grid),players,cells_filled+1,not toggle,print_grid,check_victory,ask_xy,validate_input,the_game)if check_victory(grid,players)is None and cells_filled<9 else check_victory(grid,players))[1])

If you can't read any of this, don't worry, I can't either.

You can find the original code and a slightly more readable version on my gitlab: https://gitlab.com/Rijaja/gaae/-/tree/main/tttaae (but careful, the game is in French)

[monado-stew]

took away too big a hit and it's made me realize what a monoid is and how monads relate to them

[moose-mousse]

I am writing in python rather than the pre 89 C shitshow at work right now..

And... I am just enjoying mixing function and object oriented design. Procedural mixed with imperative.

Just... making complex machines by swimming through the wonderfull sea of code in a modern langauge

[commieclimbercatboy]

Functional programming is really cool right up to the point you learn about monads. We have this beautiful way of writing code completely stateless, but then we realise that state is useful sometimes, and instead of saying "functional programming is useful but not for everything, we can use it as a tool in the toolbag among other techniques", they introduce state in the worst way possible.

[lady-inkyrius]

[Source]

[xeter-group]

classical logic vs intuitionistic logic

When I first heard about intuitionistic logic I was kind of confused. To quickly recap, classical logic is what we call 'normal logic' that you might have been taught in school. We have our AND, our OR, our NOTs, and so on. We also have some laws. For example, NOT (NOT (x)) is the same as x. When I learned about classical logic I thought it was obvious. What else could logic mean? But there are other logics, like intuitionistic logic. Intuitionistic logic *rejects* deducing x from NOT (NOT (x)). What does that even mean??? How does it make sense for NOT (NOT (x)) to be something other than x? What do you mean, "different logic"???? Thats nonsense!

The issue is that I had no idea about the difference between "syntax" and "semantics". In my introductory logic class I was taught there are two ways to prove logical statements - I can draw a big truth table, or I can use the laws of logical inference. The truth table is just me taking a logical formula and substituting in different truth values, and evaluating the operators. The laws of logical inference is applying a sequence of laws like "a AND b = b AND a" and "a AND a = a".

From a formal perspective, these are actually very different. The laws of logical inference are what are called "syntactic rules". That is, you don't need to assign a value to the terms you are operating on. You don't even need to know they represent truth values. You can just manipulate them formally. Using a big truth table is relying on what is called the "semantics" of the logic. That is, you need to remember that a term is either true or false, you need to remember the definitions of "AND" and "OR", and so on.

But there is something interesting about the syntactic rules.

There is nothing inherently "logic-ey" about them. There is nothing thats necessarily "TRUE" or "FALSE". There is a symbol for a tautology, a symbol for a contradiction, and so on, but the only reason we call them tautology or contradiction is because of their behaviour with AND and OR. The ideas of "TRUE" and "FALSE" that we are used to are just one *interpretation* of the rules of classical logic. That is, the laws of logical inference tell us how we can manipulate symbols on a page to 'deduce' things. They are a series of rules, or axioms if you wish, governing a set of values (which we may or may not choose to be TRUE and FALSE) and functions (which we may or may not choose to be NOT, AND, OR). The normal ideas of TRUE, FALSE, AND, NOT, and OR (called boolean logic) are meanings that we can substitute into the aforementioned manipulations that are consistent with them. (For whose who know what a model is, the syntactic rules are a theory, and boolean logic is a model of it.)

Isn't it interesting then that the things you can prove with the laws of logical inference are exactly the same as the things you can prove with a truth table, then? Maybe not. After all, we could just add deduction laws that are true (with respect to boolean logic) until we could prove everything we wanted to. For example, if we can't prove two things are equal that *should* be equal, just made the fact those two are equal a new law of logical inference. But what system do we get if we remove a "load bearing" law? For example, what if we no longer require that NOT (NOT (x)) = x? We would have a weaker system of axioms. We call this intuitionistic logic.

To be clear, you are still allowed to have a system for which that is true. Boolean logic is still a valid meaning to assign to intuitionistic logic, you just can't prove every statement of it. But are there any other interesting systems that satisfy this weaker set of laws? Can we call them "logic"?

Well I don't THINK of them as logic in the sense that they don't talk about truth. Instead the way to think about it is that classical logic is a set of laws that talk about truth, whereas intuitionistic logic is a set of laws that talk about constructability, or provability. For example, a statement is still either true or false. It is "obviously" always true that a statement is true or false. But it is not obviously true that a statement is either provable or disprovable. It is not necessarily true that you can either construct a proof or a counterexample.

Going back to "NOT NOT x = x". Lets say that "x" means "I can prove x", and "NOT x" means "I can disprove x". If I can disprove the fact that you can disprove x, that does not automatically mean that you can prove x. Maybe you can't prove or disprove it. Its still either true or false, we just can't prove it. This is a *different* interpretation of "NOT" and the term "x" that satisfies the rules of intuitionistic logic, but not classical logic. Note that if I can prove x, then I can definitely disprove the fact that you can disprove it. You just can't go the other way around.

So what is true (read: provable) in intuitionistic logic? You can't prove anything in intuitionistic logic that you can't prove in classical logic, because every valid law of deduction in intuitionistic logic is a valid law of classical logic. So we are able to prove strictly fewer things.

Why might we want to do this, then? In the realm of pure maths we often don't care about statements that are not decidable. Well that changes if we are working with a programming language. If I want to construct a function that returns me a value of some type, I want to see the actual value of the type. If I called a function and it just reassured me that there is an output value I'm looking for, I wouldn't be too happy about that. This links into type theory, computer proofs via types, and functional programming. It turns out there is a correspondance between computer programs (with types) and proofs in intuitionistic logic! Its called the "Curry Howard Correspondance". We think of every statement of logic corresponding to a type, and every proof of a statement corresponds to a value of that type. The details are below for those who are interested in computer types, and is pitched more for functional programming inclined people, and assumes some haskell to fully understand it, but is technically self contained?

An implication between two statements corresponds to a function between the two types. TRUE is any type that is inhabited, such as a "unit" type containing one element called (). FALSE is the type containing no values, called Void. NOT x is a function x -> Void. AND is the tuple type, and OR is the disjoint union (Either) type. For example if we have two types A and B, we can form a product type A x B, which has inhabitants of pairs (a,b) where a is type A and b is type B. Similarly we can form A | B which has inhabitants that are either Left a or Right b, where a is of type A and b is of type B.

The statement that A AND B is equivalent to B AND A is the fact that we can construct functions A x B -> B x A and B x A -> A x B, given by the swapping function (a, b) |-> (b,a). The statement that A AND TRUE is equivalent to A can be rethought of as the fact that there are functions between the types A and A x (), given by a |-> (a, ()) and (a, _) |-> a. The statement that A AND FALSE is equivalent to FALSE is the statement that A x Void has no elements.

The statement that NOT NOT x does not imply x is equivalent to the statement that there is no function with type ((x -> Void) -> Void) -> x. Imagine trying to construct such a function. You can't. You don't have any way to produce an x. Note that you can very easily create a function x -> ((x -> Void) -> Void). Thats just function application. Neat, huh?

Another interesting application of the difference between semantics and syntax in programming languages is Conal Elliott's "Compiling to Categories" paper, where he reinterprets the syntax of the programming language haskell to talk about different kinds of functions and objects.

[loonycrazy123]

I have decided in order to pass functional programming class(Haskell) I will be delusional..

Haskell is wondeful programming language which I love very much.

[american-baidu-yandex-contact]

Functional Programming

[ladyargento]

Lambdas, Functional Interfaces and Generics in Java

I wrote a little blog post on lambdas, functional interfaces and generics in Java, check it out on my dev.to blog here:

[perfectly-abnormal-1]

Yearning for module type signatures

Stolen from my twitter; hoping itll get more interaction here

I've narrowed down my yearning to this; I do not pine for specific attributes of individuals, but for situations; I wish for specific scenarios, environments, etc as a baseline; my yearning for people can be summed up by "would they be found in these scenarios i wish for?"

There is no specific attribute of a human that I directly look or wish for; which is why i Like the abstract module type signature -> module that implements said signature metaphor. It just works!

All that is to say; what if you were a module that implemented the module type I wanted and i was a functor and i took you as input

[minnesota2014]

slanderous lies on Wikipedia *smh* *smh*

[anna328p]

worldbuilding: NQ systems are written in a purely functional, dependently typed theorem prover and programming language called Rjaba. The name is a reference to an East Slavic folktale about a hen who laid a golden egg; this theme seems to have historical significance, though the exact context for the reference seems to have been lost to link-rot.

The syntax and semantics of Rjaba have a passing resemblance to historically important programming languages like Idris, Prolog, Lua, and Unison.

Headless systems tend to expose a command-line interface over a serial port. This CLI accepts a set of imperative commands and also acts as an Rjaba REPL.

Users of other languages tend to find Rjaba obtuse, difficult to mentally model, and underdocumented. Enthusiasts attempt to demonstrate its virtues at every opportunity given.

Here's a summary of the syntax that's been used in these documents so far. (The colors and formatting have significance.)

General

a : A

Asserts that a is a term of type A.

a = b

Asserts that a is equal to b.

λa. f a

A unary function that takes one argument a and returns the result of applying the function f to a.

Interactive contexts

(CLIs, REPLs, etc.)

g:Name

Identifier for the value called Name in the visible global context.

a := b

For the current interactive context, redefines the identifier a to value b.

(more to come!)

[perigordtruffle]

Does anyone else use `=<<` more than `>>=`

[vanilla-voyeur]

Very amused every time someone discovers the ultimate way to do OOP in its truest, most polymorphic, most object-oriented form and its just immutable classes with public instance variables and no methods and no inheritance being transformed through singleton classes with no instance variables and one side-effect-free method, potentially taking a function as a parameter or returning another single method class. Brother you just reinvented functional programming.

[billloguidice]

Become a better coder by harnessing math and deep learning

Become a better coder by harnessing math and deep learning #sale #math #programming #coding #education #mathematics #maths #algorithms #cryptography #datastructures #book #books

Level up your programming fundamentals with one of these great bundle options, available here. Dive into math, machine learning, and other crucial disciplines and take your programming skills to the next level! The latest bundle from Manning Publications will help you harness math to write better code, utilize deep learning across various languages and applications, and get up to speed on…

[lady-inkyrius]

I think I've written before about how I suspected functional programming is often taught badly, and I've at least got one data point to support that.

We're only doing FP properly for 2 weeks, and after the first lecture he just put up the work which was basically write a few common list functions from scratch, with no surrounding context or anything, so loads of people in the workshop were struggling because the only lecture we've had on it was the basic syntax of Erlang and not how to actually write in a functional style.